(declare-fun v1 () Bool)
(declare-fun i11 () Int)
(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(push)
(assert (or true (str.prefixof str4 (str.++ (str.++ str7 str7) (str.from_int 1)))))
(assert (> i11 43))
(assert (or (distinct str3 "" str6 (str.++ str5 (str.from_int i11))) (and v1 (= str4 (str.++ str4 str2)) (= str5 (str.++ str7 str4)) (= str2 (str.++ str6 str2)))))
(check-sat)
(push)
(assert (or v1 (str.contains (str.++ str7 str5) str6)))
(check-sat)
(assert (not (= str6 str4)))
(check-sat)
